$\forall$$r$:CRng, $a$:Ideal($r$)\{i\}, $d$:detach\_fun($\mid$$r$$\mid$;$a$).
\\[0ex]($\forall$$w$:$\mid$$r$$\mid$. SqStable($a$($w$)))
\\[0ex]$\Rightarrow$ ($\forall$$u$, $v$:$\mid$$r$$\mid$. ([$u$]\{$\mid$$r$ / $d$$\mid$\} = [$v$]\{$\mid$$r$ / $d$$\mid$\} $\in$ $\mid$$r$ / $d$$\mid$) $\Leftarrow\!\Rightarrow$ ($a$($u$ +$r$ ({-}$r$($v$)))))